#-*- coding: utf-8 -*-
"""
Basic K-calculuses structures.

Usage example:

>>> from KBasic import *
>>> B = Basis()
>>> cat = InformationUnit(B, B.object, 'кошка')
>>> dog = InformationUnit(B, B.object, 'собака')
>>> cat_n_dog = KAnd([cat, dog])
>>> cat_n_dog
<KBasic.KAnd object at 0xb732128c>
>>> print(cat_n_dog)
кошка & собака
>>> print(cat_n_dog.type)
[ob]
>>> print(cat_n_dog.rule)
7
"""

from ktypes import *
from abc import abstractmethod
import sys
from itertools import chain

def c2(char_code, analog_string):
    try:
        return unichr(char_code).encode(locale.getpreferredencoding())
    except:
        return analog_string
    
if sys.version < "3":
    # Python 2.*
    import locale
    from itertools import imap, izip
    ck_neg = c2(0x00AC, ' ~')
    ck_and = c2(0x2227, ' & ')
    ck_or = c2(0x2228, ' V ')
    ck_eq = c2(0x2261, ' = ')
    ck_concept = c2(0xE123, ' ^')
    ck_forall = c2(0x2200, ' for all ')
    ck_exists = c2(0x2203, ' exists ')
    ck_int1 = 'int' + c2(0x2081, '1')
    ck_int2 = 'int' + c2(0x2082, '2')
else:
    # Python 3.*
    imap = map
    izip = zip
    ck_neg = '\u00AC'
    ck_and = '\u2227'
    ck_or = '\u2228'
    ck_eq = '\u2261'
    ck_concept = '\uE123'
    ck_forall = '\u2200'
    ck_exists = '\u2203'
    ck_int1 = 'int\u2081'
    ck_int2 = 'int\u2082'

class Basis(kobject):
    """Class for definition of conceptual basis
    
    Attributes:
        Universum = kdict()
            Primary universum set
        Variables = kdict()
            Variables set    
        Sorts = kset()
            Sorts (primary types) set
        GenSet = kset()
            Generalization relation set
        entity = TSort(self, '[ent]')
            Entity type - most general type
        concept= TSort(self, '[con]')
            Concept type - base type for concepts
        object=TSort(self, '[ob]')
            Object type - base type for objects (all except concepts and some special types)
        proposal = TSort(self,'P')
            Type for proposals
        binlog = TSort(self, 'binlog')
            Type binary logic operations: ∧, ∨ 
        int1 = TSort(self, ck_int1)
            Type for intentional quantifiers
        int2 = TSort(self, ck_int2)
            Type for intentional quantifiers
        ext = TSort(self, 'ext')
            Type for extentional quantifiers: ∀, ∃
        neg = TSort(self, 'neg')
            Type for negative symbol: ¬
        k_and = InformationUnit(self, self.binlog, ck_and)
            Universum item ∧
        k_or = InformationUnit(self, self.binlog, ck_or)
            Universum item ∨
        k_neg = InformationUnit(self, ck_neg, self.neg)
            Universum item ¬
        k_forall = InformationUnit(self, self.ext, ck_forall)
            Universum item ∀
        k_exists = InformationUnit(self, self.ext, ck_exists)
            Universum item ∃
    """

    def __init__(self):
        self.Universum = kdict()
        self.Variables = kdict()
        """Primary universum set"""
        self.Sorts = kset()
        self.GenSet = kset()
        self.entity = TSort(self, '[ent]')
        self.concept= TSort(self, '[con]')
        self.object=TSort(self, '[ob]') 
        self.proposal = TSort(self,'P')
        self.binlog = TSort(self, 'binlog')
        self.int1 = TSort(self, ck_int1)
        self.int2 = TSort(self, ck_int2)
        self.ext = TSort(self, 'ext')
        self.neg = TSort(self, 'neg')
        self.k_and = InformationUnit(self, ck_and, self.binlog)
        self.k_or = InformationUnit(self, ck_or, self.binlog)
        self.k_neg = InformationUnit(self, ck_neg, self.neg)
        self.k_forall = InformationUnit(self, ck_forall, self.ext)
        self.k_exists = InformationUnit(self, ck_exists, self.ext)
        
    def Generalization(self, left, right):
        return (left == right) or ((left, right) in self.GenSet)


class UniversumItem(kobject):
    """Base class for primary universum items
    
        Attributes:
            basis - link to conceptual basis
            type - type of universum item
    
    """

    def __init__(self, basis, type):
        kobject.__init__(self)
        self.basis = basis
        self.type = type
        
class EAlreadyInBasis(Exception):
    """Exception raised if application trying add universum item or variable
    with already existed symbolic representation
    """
    def __init__(self, text=''):
        self.text = text

    def __str__(self):
        Error = "Item already exists in basis"
        if self.text:
            return Error + ": " + self.text

        else:
            return Error

class InformationUnit(UniversumItem):
    """Class for information units: objects, relations, functions, etc
    
        Attribute:

        repr - attribute contains string representation of information unit
    
    """
    def __init__(self, basis, text, type):
        UniversumItem.__init__(self, basis, type)
        self.text = text
        if text in basis.Universum:
            raise EAlreadyInBasis(text)
        else:
            basis.Universum[text] = self        

    def __str__(self):
        return self.text

class TSort(InformationUnit):
    def __init__(self, basis, text):
        InformationUnit.__init__(self, basis, text, TConcept(self))
        basis.Sorts.add(self)

    def __le__(self, right):
        if self == self.basis.entity:
            return true
        elif self == self.basis.concept:
            return isinstance(right, TConcept)
        elif self == self.basis.object:
            return not isinstance(right, TConcept)
        elif isinstance(right, TSort):
            return self.basis.Generalization(self, right)
        elif isinstance(right, TElementary):
            return self in right.items
        else:
            return False
        
##    def __eq__(self, right):
##        return self == right
     

class Function(InformationUnit):
    """Class for K-functions
    
        Attributes:
            arg_types - list of argument types
            res_type - type of function result
    """
    
    def __init__(self, basis, name, arg_types, res_type):
        InformationUnit.__init__(self, basis, name, TSet(TSequence(arg_types + [res_type])))
        self.arg_types = arg_types
        self.res_type = res_type
        
class Relation(InformationUnit):
    """Class for K-relations
        Attribute:
            arg_types - list of argument types
    """

    def __init__(self, basis, name, arg_types):
        InformationUnit.__init__(self, basis, name, TSet(TSequence(arg_types)))
        self.arg_types = arg_types

class Variable(UniversumItem):
    """Class for K-variables
        Attributes:
            name - name of variable (text representation)
            reference - link to K-formula defined by this variable
    """
    
    def __init__(self, basis, name, type):
        UniversumItem.__init__(self, basis, type)
        self.name = name
        referense = None        
        if name in basis.Variables:
            raise EAlreadyInBasis(name)
        else:
            basis.Variables[name] = self        

    def __str__(self):
        return str( self.name )

def is_variable(obj):
    """true if obj is K-variable"""
    return isinstance(obj, Variable)

def is_function(obj):
    """true if obj is K-function"""
    return isinstance(obj, Function)

def is_relation(obj):
    """true if obj is K-relation"""
    return isinstance(obj, Relation)

def is_concept(obj):
    """true if obj is concept"""
    return isinstance(obj.type, TConcept)

class TConcept(kobject):
    """Class for concept types: T
        Attribute:
        item - subtype (sort or more complex type)
    """
    def __init__(self, item):
        self.item=item
    
    def __le__(self, right):
        if isinstance(right, TConcept):
            return self.item <= right.item
        else:
            return False

    def __eq__(self, right):
        if isinstance(right, TConcept):
            return self.item == right.item
        else:
            return False

    def __hash__(self):
        return hash(self.item)

    def __str__(self):
        return ck_concept + str(self.item)

class TElementary(kobject):
    """Class for elementary complex types: T1*T2*...*Tn
        Attribute:
            items - subtypes        
    """
    
    def __init__(self, items):
        self.items = set(items)

    def __le__(self, right):
        if isinstance(right, TElementary):
            return self.items == right.items
        else:
            return False
     
    def __eq__(self, right):
        if isinstance(right, TElementary):
            return self.items == right.items
        else:
            return False

    def __str__(self):
        return "*".join(map(str, self.items))

class TSequence(kobject):
    """Class for sequence types: (T1, T2, ..., Tn)
        Attribute:
            items - subtypes        
    """
    def __init__(self, items):
        self.items = items

    def __le__(self, right):
        if isinstance(right, TSequence):
            return all(lambda x: (x[0] <= x[1]), izip(self.items,right.items))
        else:
            return False
     
    def __eq__(self, right):
        if isinstance(right, TSequence):
            return all(lambda x: (x[0] == x[1]), izip(self.items,right.items))
        else:
            return False
            
    def __hash__(self):
        return hash(tuple(self.items))

    def __str__(self):
        return '(' + ','.join(map(str,self.items)) + ')'

class TSet(kobject):
    """Class for set types: {T1}
        Attribute:
            items - subtype        
    """
    def __init__(self, item):
        self.item = item

    def __le__(self, right):
        if isinstance(right, TSet):
            return self.item <= right.item
        else:
            return False

    def __eq__(self, right):
        if isinstance(right, TSet):
            return self.item == right.item
        else:
            return False

    def __hash__(self):
        return hash(self.item)
        
    def __str__(self):
        return '{' + str(self.item) + '}'


class KFormula(kobject):
    """Abstract (base) class for K-formulas and subformulas
        Attribute:
            owner - formula contained this one
    """
    def __init__(self):
        self.owner = None
        
    def __eq__(self, right):
        return (self.__class__ == right.__class__) and not cmp(self.parts, right.parts)

    def __hash__(self):
        return hash(tuple(self.parts))
        
    @property
    @abstractmethod
    def rule(self):
        """Constraction rule number"""
        pass

    @property
    @abstractmethod
    def type(self):
        """Formula type"""
        pass

    @property
    @abstractmethod
    def parts(self):
        """Parts of formula"""
        pass

    @property
    def basis(self):
        """Conceptual basis for formula"""
        return self.parts[0].basis

class EFormulaBuild(Exception):
    """Formula building error exception"""
    
    def __init__(self, text=''):
        self.text = text

    def __str__(self):
        Error = "K-formula building error"
        if self.text:
            return Error + ": " + self.text
        else:
            return Error

class KAtom(KFormula):
    """Atomic formulas: universum items and variables"""
    def __init__(self, item):
        KFormula.__init__(self)
        if not isinstance(item, UniversumItem):
            raise EFormulaBuild(str(item) + ' is not universum item')
        self.item = item
        
    def __eq__(self, right):
        return (type(self) == type(right)) and (self.item==right.item)

    def __hash__(self):
        return hash(self.item)
        
    @property
    def rule(self):
        return 0

    @property
    def type(self):
        return self.item.type
    
    @property
    def parts(self):
        return []

    def __str__(self):
        return str(self.item)

    @property
    def basis(self):
        return self.item.basis

def f(item, owner = None):
    """Service function
    return item if it's already formula or atomic formula for univerum item or variable else
    Also set result formula owner attribute to owner parameter
    """
    if isinstance(item, KFormula):
        Result = item
    else:
        Result = KAtom(item)
    if owner:
        Result.owner = owner
    return Result
    
def flist(items, owner = None):
    """Service function
    return list of items processed by f - function (see above)
    """
    return klist( imap( lambda x: f(x, owner), items) )

def fset(items, owner = None):
    return kset( imap( lambda x: f(x, owner), items) )

def fdict(items, owner = None):
    return kdict( (f(k), f(v, owner)) for k, v in items.items() )

class KIntentionalQuantifier(KFormula):
    def __init__(self, quantifier, concept):
        KFormula.__init__(self)

        self.quantifier = f(quantifier, self)
        if not isinstance(concept.type, TConcept):
            raise EFormulaBuild(str(concept) + ' is not concept')
        self.concept = f(concept, self)

    @property
    def rule(self):
        return 1

    @property
    def type(self):
        if self.quantifier.item.type == self.basis.int1:
            return self.concept.type.item
        if self.quantifier.item.type == self.basis.int2:
            return TSet(self.concept.type.item)
        raise EFormulaBuild(str(self.quantifier.item) + 'is not intentional quantifier')

    @property
    def parts(self):
        return [self.quantifier, self.concept]

    def __str__(self):
        return str(self.quantifier) + ' ' + str(self.concept)

class KFunction(KFormula):
    def __init__(self, function, arguments):
        KFormula.__init__(self)

        if not is_function(function):
            raise EFormulaBuild(str(function) + ' is not function')
        self.function = f(function, self)

        self.arguments = flist(arguments, self)
        arg_types = self.function.item.arg_types

        if len(arg_types) != len(arguments):
            raise EFormulaBuild('argument count (%d) does not match dimention of argument list (%d)' % ( len(arguments), len(arg_types) ))
        for arg, type in izip(self.arguments, arg_types):
            if not (type <= arg.type):
                raise EFormulaBuild('type of argument %s - %s - does not match type %s or specialize it' % ( str(arg), str(arg.type), str(type) ))

    @property
    def rule(self):
        return 2

    @property
    def type(self):
        return self.function.item.res_type
    
    @property
    def parts(self):
        return [self.function] + self.arguments

    def __str__(self):
        return str(self.function) + '(' + ','.join(map(str, self.agruments)) + ')'

class KRelation(KFormula):
    def __init__(self, relation, arguments):
        KFormula.__init__(self)

        if not is_relation(relation):
            raise EFormulaBuild(str(relation) + ' is not relation')
        self.relation = f(relation, self)

        arg_types = self.relation.item.arg_types
        self.arguments = flist(arguments, self)

        if len(arg_types) != len(arguments):
            raise EFormulaBuild('argument count (%d) does not match relation dimention (%d)' % ( len(arguments), len(arg_types) ))
        for arg, arg_type in izip(self.arguments, arg_types):
            if not (arg_type <= arg.type):
                raise EFormulaBuild('type of argument %s - %s - does not match type %s or specialize it' % ( str(arg), str(arg.type), str(type) ))

    @property
    def rule(self):
        return 4

    @property
    def type(self):
        return self.basis.proposal
    
    @property
    def parts(self):
        return [self.relation] + self.arguments

    def __str__(self):
        return str(self.relation) + '(' + ','.join(map(str, self.arguments)) + ')'

class KEquals(KFormula):
    def __init__(self, left, right):
        KFormula.__init__(self)
        if left.type != right.type:
            raise EFormulaBuild('types of %s and %s must be equals' % (str(left), str(right)))
        self.left = f(left, self)
        self.right = f(right, self)

    @property
    def rule(self):
        return 3

    @property
    def type(self):
        return self.basis.proposal
    
    @property
    def parts(self):
        return [self.left, self.right]

    def __str__(self):
        return str(left) + ck_eq + str(right)

class KVarAssignment(KFormula):
    def __init__(self, item, variable):
        KFormula.__init__(self)
        self.item = f(item)
        if not is_variable(variable):
            raise EFormulaBuild("%s is not variable" % str(variable))
        variable.referense = item
        self.variable = f(variable)        

    @property
    def rule(self):
        return 5

    @property
    def type(self):
        return self.item.type
    
    @property
    def parts(self):
        return [self.item, self.variable]

    def __str__(self):
        return str(self.item) + ':' + str(self.variable)

class KNegative(KFormula):
    def __init__(self, item):
        KFormula.__init__(self)
        self.item = f(item, self)
    
    @property
    def rule(self):
        return 6

    @property
    def type(self):
        return self.item.type
    
    @property
    def parts(self):
        return [self.item]

    def __str__(self):
        return ck_neg + str(self.item)

class KBinLogic(KFormula):
    def __init__(self, items):
        KFormula.__init__(self)
        self.items = flist(items, self)

    @property
    def rule(self):
        return 7

    @property
    def type(self):
        return self.items[0].type

    @property
    def parts(self):
        return self.items

    @abstractmethod
    def logicOperation(self):
        pass

    def __str__(self):
        return self.logicOperation().join(map(str,self.items))

class KAnd(KBinLogic):
    def logicOperation(self):
        return ck_and

class KOr(KBinLogic):
    def logicOperation(self):
        return ck_or

class KConcept(KFormula):
    def __init__(self, concept, conditions):
        KFormula.__init__(self)
        if not is_concept(concept):
            raise EFormulaBuild("%s is not concept" % str(concept))
        self.concept = f(concept)
        self.conditions = fdict(conditions, self)

    @property
    def rule(self):
        return 8

    @property
    def type(self):
        return self.concept.type

    @property
    def parts(self):
        return [self.concept] + list( chain( *(self.conditions.items()) ) )

    def __str__(self):
        return str(self.concept) + '*' + ''.join(map(lambda x: '(' + str(x[0]) + ',' + str(x[1]) + ')', self.conditions.items()))

class KExtentionalQuantifier(KFormula):
    def __init__(self, quantifier, variable, concept, proposition):
        KFormula.__init__(self)
        self.quantifier = quantifier
        if not is_concept(concept):
            raise EFormulaBuild("%s is not concept" % str(concept))
        self.concept = f(concept, self)
        if not is_variable(variable):
            raise EFormulaBuild("%s is not variable" % str(variable))
        self.variable = f(variable, self)
        self.proposition = f(proposition, self)

    @property
    def rule(self):
        return 9

    @property
    def type(self):
        return self.basis.proposal
    
    @property
    def parts(self):
        return [self.variable, self.concept, self.proposition]

    def __str__(self):
        return str(self.quantifier) + str(self.variable) + '(' + str(self.concept) + ')' + str(self.proposition)

class KOrderedList(KFormula):
    def __init__(self, items):
        KFormula.__init__(self)
        self.items = flist(items, self)

    @property
    def rule(self):
        return 10

    @property
    def type(self):
        return TSequence( map(lambda x: x.type, self.items ) )

    @property
    def parts(self):
        return self.items

    def __str__(self):
        return '<' + ','.join(map(str,self.items)) + '>'

p0 = KAtom
p1 = KIntentionalQuantifier
p2 = KFunction
p3 = KEquals
p4 = KRelation
p5 = KVarAssignment
p6 = KNegative
p7and = KAnd
p7or = KOr
p8 = KConcept
p9 = KExtentionalQuantifier
p10 = KOrderedList

